Nuprl Definition : ma-ef-val
0,22
postcript
pdf
M
.ef(
k
,
x
,
s
,
v
)?
w
== 1of(2of(2of(2of(2of(
M
)))))(<
k
,
x
>)?
s
,
v
.
w
(
s
,
v
)
latex
clarification:
M
.ef(
k
,
x
,
s
,
v
)?
w
== fpf-cap(1of(2of(2of(2of(2of(
M
)))));product-deq(Knd;Id;KindDeq;IdDeq);<
k
,
x
>;
s
,
v
.
w
)(
s
,
v
)
latex
Definitions
M
.ef(
k
,
x
,
s
,
v
)?
w
,
f
(
x
)?
z
,
1of(
t
)
,
2of(
t
)
,
product-deq(
A
;
B
;
a
;
b
)
,
Knd
,
Id
,
KindDeq
,
IdDeq
FDL editor aliases
ma-ef-val
origin
s,v. w(s,v)
s,v. w)(s,v) s,v. w(s,v)
s,v. w)(s,v)